Section: New Results

CISE Logic and tool for proving invariants in distributed databases

Participants : Marc Shapiro [correspondent] , Mahsa Najafzadeh, Alexey Gotsman, Carla Ferreira.

We have developed a new sound logic for proving the correctness of a distributed database under concurrent updates, showing whether the application maintains the database's integrity invariants. An operation of the application is specified as a preparator, which checks the operation's precondition at an origin replica and generates an effector. The effector abstracts the update to be applied to every replica. The application also specifies which operations are allowed to take place concurrently. In summary, the logic shows that the application maintains the invariant if the three following rules are satisfied:

• Each operation individually maintains the invariant. It follows that operations' preconditions are sufficiently strong to ensure correctness in a sequential execution.

• The effectors of any two operations that can execute concurrently commute. This implies that the database replicas all converge to the same state.

• For any pair of operations $u$ and $v$ that can execute concurrently, the precondition of $u$ is stable under the effector of $v$, and vice-versa.

This result is published at POPL 2016 [50] .

We have implemented a tool (based on the Z3 SMT solver) that implements these rules. A demo of the tool is available online [78] . If the application passes the tool, it is correct. If not, the tool returns a counter-example, which the application developer can inspect to find the source of the error. Generally speaking, the developer can either weaken the invariants or the effects of operations, or strengthen consistency by disallowing concurrency. By choosing one or the other, the developer performs a co-design of the application with its consistency protocol, in order to have the highest possible concurrency that still ensures correctness.

For instance, consider a database of bank accounts, with the invariant that an account's balance must be positive. The banking application has operations $credit(acct,amt)$, $debit(acct,amt)$, and $accrue-interest\left(acct\right)$. The first rule dictates that $debit$ has the precondition $amt=balance$. The second rule dictates that $accrue-interest$ computes the amount of interest according to the state at the origin, not at every replica. The third rule is violated if concurrent $debit$s are allowed; if the bank wishes to uphold the invariant, the only correct solution is to disallow concurrent $debit$s.